DECLARE INDVAR e ε EXPRESSION;

DECLARE PREDCONST isconst(EXPRESSION);

DECLARE PREDCONST isvar(EXPRESSION);

DECLARE PREDCONST issum(EXPRESSION);

DECLARE OPCONST s1(EXPRESSION)=EXPRESSION;

DECLARE OPCONST s2(EXPRESSION)=EXPRESSION;

DECLARE PREDPAR pred 1;

AXIOM expsyn:
	∀ e.(isconst(e)∨isvar(e)∨issum(e)),
	∀ e.(isconst(e) ∨ isvar(e) ∨ (issum(e)∧ pred(s1(e))∧pred(s2(e)))
⊃ pred(e)) ⊃ ∀ e.(pred(e));
;

DECLARE INDVAR xi ε SOURCESTATE;

DECLARE OPCONST value(EXPRESSION,SOURCESTATE) = NUMBER;

DECLARE OPCONST val(EXPRESSION) = NUMBER;

DECLARE OPCONST c(EXPRESSION,SOURCESTATE) = NUMBER;

DECLARE OPCONST plus(NUMBER,NUMBER) = NUMBER;

AXIOM expsem:
	∀ e xi.(isconst(e) ⊃ value(e,xi) = val(e)),

	∀ e xi.(isvar(e) ⊃ value(e,xi) = c(e,xi)),

	∀ e xi.(issum(e) ⊃ value(e,xi) = plus(value(s1(e),xi),value(s2(e),xi)))
;;

declare PREDCONST null(PROGRAM);

declare PREDCONST isli(PROGRAM);

declare PREDCONST isload(PROGRAM);

declare PREDCONST isadd(PROGRAM);

declare PREDCONST issto(PROGRAM);

declare OPCONST first(PROGRAM)=PROGRAM;

declare OPCONST rest(PROGRAM)=PROGRAM;

declare OPCONST append(PROGRAM,PROGRAM)=PROGRAM;

declare OPCONST mkli(NUMBER)=PROGRAM;

declare OPCONST mkload(NUMBER)=PROGRAM;


declare OPCONST mkadd(NUMBER)=PROGRAM;

declare OPCONST mksto(NUMBER)=PROGRAM;

declare OPCONST arg(PROGRAM)=NUMBER;

declare INDVAR s ε PROGRAM;

declare INDVAR t ε PROGRAM;

declare INDVAR n n1 n2 n3 ε NUMBER;

axiom progsyn:
	∀s.(¬null(s) ⊃ isli(first(s))∨isload(first(s))∨isadd(first(s))
		∨issto(first(s))),
	∀s t.(null(s) ⊃ append(s,t) = t),
	∀s t.(¬null(s) ⊃ first(append(s,t)) = first(s)),
	∀s t.(¬null(s) ⊃ rest(append(s,t)) = append(rest(s),t));;
	

axiom li:
	∀ n.(isli(mkli(n))),
	∀ n.(n = arg(mkli(n))),
	∀ n.(null(rest(mkli(n)))),
	∀ s.(isli(s) ⊃ first(s) = s);
;

axiom load:
	∀n.isload(mkload(n)),
	∀n.(n=arg(mkload(n))),
	∀n.(null(rest(mkload(n)))),
	∀s.(isload(s)⊃first(s)=s);;

axiom sto:
	∀n.issto(mksto(n)),
	∀n.(n=arg(mksto(n))),
	∀n.(null(rest(mksto(n)))),
	∀s.(issto(s)⊃first(s)=s);;

axiom add:
	∀n.isadd(mkadd(n)),
	∀n.(n=arg(mkadd(n))),
	∀n.(null(rest(mkadd(n)))),
	∀s.(isadd(s)⊃first(s)=s);;

declare INDVAR x y z x1 y1 z1 x2 y2 z2 ε NUMBER;

declare INDVAR eta eta1 eta2 eta3 ε STATE;

declare OPCONST cc(NUMBER,STATE) =NUMBER;

declare OPCONST a(NUMBER,NUMBER,STATE) = STATE;

axiom assign:
	∀x n eta.cc(x,a(x,n,eta))=n,
	∀x y n eta.(¬(x=y) ⊃ cc(x,a(y,n,eta)) = cc(x,eta)),
	∀x n1 n2 eta.a(x,n1,a(x,n2,eta)) = a(x,n1,eta),
	∀x y n1 n2 eta.(¬(x=y) ⊃ a(x,n1,a(y,n2,eta)) = a(y,n2,a(x,n1,eta))),
	∀x eta.a(x,cc(x,eta),eta) = eta;;